Nuprl Lemma : possible-event_wf
11,40
postcript
pdf
poss
:(ES{i}
{i'}). possible-event{i:l}(
poss
)
{i'}
latex
Definitions
Type
,
,
t
T
,
ES
,
x
:
A
B
(
x
)
,
f
(
a
)
,
x
:
A
.
B
(
x
)
,
E
,
x
:
A
B
(
x
)
,
PossibleEvent(
poss
)
Lemmas
es-E
wf
,
event
system
wf
origin
poss:(ES{i}
{i'}). possible-event{i:l}(poss) 
{i'} poss:(ES{i}{i'}). possible-event{i:l}(poss) {i'} TB(x)x:A. B(x)
B(x)